H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.66 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((sort :: [()] -> [()]) :: [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge

cmp xs []

merge

cmp [] ys

merge

cmp (x : xs) (y : ys)

case	x `cmp` y of
	GT	->	y : merge cmp (x : xs) ys
	_	->	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : merge cmp (x : xs) ys

_ → x : merge cmp xs (y : ys)

is transformed to

merge0 y cmp x xs ys GT = y : merge cmp (x : xs) ys

merge0 y cmp x xs ys _ = x : merge cmp xs (y : ys)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((sort :: [()] -> [()]) :: [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((sort :: [()] -> [()]) :: [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(sort :: [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sort",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sort vz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="mergesort compare vz3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="(mergesort' compare) . map wrap",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="mergesort' compare (map wrap vz3)",fontsize=16,color="burlywood",shape="box"];580[label="vz3/vz30 : vz31",fontsize=10,color="white",style="solid",shape="box"];6 -> 580[label="",style="solid", color="burlywood", weight=9];
580 -> 7[label="",style="solid", color="burlywood", weight=3];
581[label="vz3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 581[label="",style="solid", color="burlywood", weight=9];
581 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="mergesort' compare (map wrap (vz30 : vz31))",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="mergesort' compare (map wrap [])",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="mergesort' compare (wrap vz30 : map wrap vz31)",fontsize=16,color="burlywood",shape="box"];582[label="vz31/vz310 : vz311",fontsize=10,color="white",style="solid",shape="box"];9 -> 582[label="",style="solid", color="burlywood", weight=9];
582 -> 11[label="",style="solid", color="burlywood", weight=3];
583[label="vz31/[]",fontsize=10,color="white",style="solid",shape="box"];9 -> 583[label="",style="solid", color="burlywood", weight=9];
583 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="mergesort' compare []",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mergesort' compare (wrap vz30 : map wrap (vz310 : vz311))",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mergesort' compare (wrap vz30 : map wrap [])",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="[]",fontsize=16,color="green",shape="box"];14[label="mergesort' compare (wrap vz30 : wrap vz310 : map wrap vz311)",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="mergesort' compare (wrap vz30 : [])",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="mergesort' compare (merge_pairs compare (wrap vz30 : wrap vz310 : map wrap vz311))",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="wrap vz30",fontsize=16,color="black",shape="triangle"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 245[label="",style="dashed", color="red", weight=0];
18[label="mergesort' compare (merge compare (wrap vz30) (wrap vz310) : merge_pairs compare (map wrap vz311))",fontsize=16,color="magenta"];18 -> 246[label="",style="dashed", color="magenta", weight=3];
18 -> 247[label="",style="dashed", color="magenta", weight=3];
19[label="vz30 : []",fontsize=16,color="green",shape="box"];246[label="map wrap vz311",fontsize=16,color="burlywood",shape="triangle"];585[label="vz311/vz3110 : vz3111",fontsize=10,color="white",style="solid",shape="box"];246 -> 585[label="",style="solid", color="burlywood", weight=9];
585 -> 400[label="",style="solid", color="burlywood", weight=3];
586[label="vz311/[]",fontsize=10,color="white",style="solid",shape="box"];246 -> 586[label="",style="solid", color="burlywood", weight=9];
586 -> 401[label="",style="solid", color="burlywood", weight=3];
247 -> 402[label="",style="dashed", color="red", weight=0];
247[label="merge compare (wrap vz30) (wrap vz310)",fontsize=16,color="magenta"];247 -> 403[label="",style="dashed", color="magenta", weight=3];
247 -> 404[label="",style="dashed", color="magenta", weight=3];
245[label="mergesort' compare (vz34 : merge_pairs compare vz35)\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];588[label="vz35/vz350 : vz351",fontsize=10,color="white",style="solid",shape="box"];245 -> 588[label="",style="solid", color="burlywood", weight=9];
588 -> 405[label="",style="solid", color="burlywood", weight=3];
589[label="vz35/[]",fontsize=10,color="white",style="solid",shape="box"];245 -> 589[label="",style="solid", color="burlywood", weight=9];
589 -> 406[label="",style="solid", color="burlywood", weight=3];
400[label="map wrap (vz3110 : vz3111)",fontsize=16,color="black",shape="box"];400 -> 407[label="",style="solid", color="black", weight=3];
401[label="map wrap []",fontsize=16,color="black",shape="box"];401 -> 408[label="",style="solid", color="black", weight=3];
403 -> 17[label="",style="dashed", color="red", weight=0];
403[label="wrap vz310",fontsize=16,color="magenta"];403 -> 409[label="",style="dashed", color="magenta", weight=3];
404 -> 17[label="",style="dashed", color="red", weight=0];
404[label="wrap vz30",fontsize=16,color="magenta"];402[label="merge compare vz37 vz36",fontsize=16,color="burlywood",shape="triangle"];592[label="vz36/vz360 : vz361",fontsize=10,color="white",style="solid",shape="box"];402 -> 592[label="",style="solid", color="burlywood", weight=9];
592 -> 410[label="",style="solid", color="burlywood", weight=3];
593[label="vz36/[]",fontsize=10,color="white",style="solid",shape="box"];402 -> 593[label="",style="solid", color="burlywood", weight=9];
593 -> 411[label="",style="solid", color="burlywood", weight=3];
405[label="mergesort' compare (vz34 : merge_pairs compare (vz350 : vz351))\n  Ord a",fontsize=16,color="burlywood",shape="box"];594[label="vz351/vz3510 : vz3511",fontsize=10,color="white",style="solid",shape="box"];405 -> 594[label="",style="solid", color="burlywood", weight=9];
594 -> 412[label="",style="solid", color="burlywood", weight=3];
595[label="vz351/[]",fontsize=10,color="white",style="solid",shape="box"];405 -> 595[label="",style="solid", color="burlywood", weight=9];
595 -> 413[label="",style="solid", color="burlywood", weight=3];
406[label="mergesort' compare (vz34 : merge_pairs compare [])\n  Ord a",fontsize=16,color="black",shape="box"];406 -> 414[label="",style="solid", color="black", weight=3];
407[label="wrap vz3110 : map wrap vz3111",fontsize=16,color="green",shape="box"];407 -> 415[label="",style="dashed", color="green", weight=3];
407 -> 416[label="",style="dashed", color="green", weight=3];
408[label="[]",fontsize=16,color="green",shape="box"];409[label="vz310",fontsize=16,color="green",shape="box"];410[label="merge compare vz37 (vz360 : vz361)",fontsize=16,color="burlywood",shape="box"];596[label="vz37/vz370 : vz371",fontsize=10,color="white",style="solid",shape="box"];410 -> 596[label="",style="solid", color="burlywood", weight=9];
596 -> 417[label="",style="solid", color="burlywood", weight=3];
597[label="vz37/[]",fontsize=10,color="white",style="solid",shape="box"];410 -> 597[label="",style="solid", color="burlywood", weight=9];
597 -> 418[label="",style="solid", color="burlywood", weight=3];
411[label="merge compare vz37 []",fontsize=16,color="black",shape="box"];411 -> 419[label="",style="solid", color="black", weight=3];
412[label="mergesort' compare (vz34 : merge_pairs compare (vz350 : vz3510 : vz3511))\n  Ord a",fontsize=16,color="black",shape="box"];412 -> 420[label="",style="solid", color="black", weight=3];
413[label="mergesort' compare (vz34 : merge_pairs compare (vz350 : []))\n  Ord a",fontsize=16,color="black",shape="box"];413 -> 421[label="",style="solid", color="black", weight=3];
414[label="mergesort' compare (vz34 : [])\n  Ord a",fontsize=16,color="black",shape="box"];414 -> 422[label="",style="solid", color="black", weight=3];
415 -> 17[label="",style="dashed", color="red", weight=0];
415[label="wrap vz3110",fontsize=16,color="magenta"];415 -> 423[label="",style="dashed", color="magenta", weight=3];
416 -> 246[label="",style="dashed", color="red", weight=0];
416[label="map wrap vz3111",fontsize=16,color="magenta"];416 -> 424[label="",style="dashed", color="magenta", weight=3];
417[label="merge compare (vz370 : vz371) (vz360 : vz361)",fontsize=16,color="black",shape="box"];417 -> 425[label="",style="solid", color="black", weight=3];
418[label="merge compare [] (vz360 : vz361)",fontsize=16,color="black",shape="box"];418 -> 426[label="",style="solid", color="black", weight=3];
419[label="vz37",fontsize=16,color="green",shape="box"];420[label="mergesort' compare (vz34 : merge compare vz350 vz3510 : merge_pairs compare vz3511)\n  Ord a",fontsize=16,color="black",shape="box"];420 -> 427[label="",style="solid", color="black", weight=3];
421[label="mergesort' compare (vz34 : vz350 : [])\n  Ord a",fontsize=16,color="black",shape="box"];421 -> 428[label="",style="solid", color="black", weight=3];
422[label="vz34\n  Ord a",fontsize=16,color="green",shape="box"];423[label="vz3110",fontsize=16,color="green",shape="box"];424[label="vz3111",fontsize=16,color="green",shape="box"];425 -> 467[label="",style="dashed", color="red", weight=0];
425[label="merge0 vz360 compare vz370 vz371 vz361 (compare vz370 vz360)",fontsize=16,color="magenta"];425 -> 468[label="",style="dashed", color="magenta", weight=3];
425 -> 469[label="",style="dashed", color="magenta", weight=3];
425 -> 470[label="",style="dashed", color="magenta", weight=3];
425 -> 471[label="",style="dashed", color="magenta", weight=3];
425 -> 472[label="",style="dashed", color="magenta", weight=3];
426[label="vz360 : vz361",fontsize=16,color="green",shape="box"];427[label="mergesort' compare (merge_pairs compare (vz34 : merge compare vz350 vz3510 : merge_pairs compare vz3511))\n  Ord a",fontsize=16,color="black",shape="box"];427 -> 430[label="",style="solid", color="black", weight=3];
428[label="mergesort' compare (merge_pairs compare (vz34 : vz350 : []))\n  Ord a",fontsize=16,color="black",shape="box"];428 -> 431[label="",style="solid", color="black", weight=3];
468[label="vz361",fontsize=16,color="green",shape="box"];469[label="compare vz370 vz360",fontsize=16,color="burlywood",shape="triangle"];601[label="vz370/()",fontsize=10,color="white",style="solid",shape="box"];469 -> 601[label="",style="solid", color="burlywood", weight=9];
601 -> 488[label="",style="solid", color="burlywood", weight=3];
470[label="vz371",fontsize=16,color="green",shape="box"];471[label="vz370",fontsize=16,color="green",shape="box"];472[label="vz360",fontsize=16,color="green",shape="box"];467[label="merge0 vz44 compare vz45 vz46 vz47 vz48\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];602[label="vz48/LT",fontsize=10,color="white",style="solid",shape="box"];467 -> 602[label="",style="solid", color="burlywood", weight=9];
602 -> 489[label="",style="solid", color="burlywood", weight=3];
603[label="vz48/EQ",fontsize=10,color="white",style="solid",shape="box"];467 -> 603[label="",style="solid", color="burlywood", weight=9];
603 -> 490[label="",style="solid", color="burlywood", weight=3];
604[label="vz48/GT",fontsize=10,color="white",style="solid",shape="box"];467 -> 604[label="",style="solid", color="burlywood", weight=9];
604 -> 491[label="",style="solid", color="burlywood", weight=3];
430 -> 245[label="",style="dashed", color="red", weight=0];
430[label="mergesort' compare (merge compare vz34 (merge compare vz350 vz3510) : merge_pairs compare (merge_pairs compare vz3511))\n  Ord a",fontsize=16,color="magenta"];430 -> 433[label="",style="dashed", color="magenta", weight=3];
430 -> 434[label="",style="dashed", color="magenta", weight=3];
431 -> 245[label="",style="dashed", color="red", weight=0];
431[label="mergesort' compare (merge compare vz34 vz350 : merge_pairs compare [])\n  Ord a",fontsize=16,color="magenta"];431 -> 435[label="",style="dashed", color="magenta", weight=3];
431 -> 436[label="",style="dashed", color="magenta", weight=3];
488[label="compare () vz360",fontsize=16,color="burlywood",shape="box"];607[label="vz360/()",fontsize=10,color="white",style="solid",shape="box"];488 -> 607[label="",style="solid", color="burlywood", weight=9];
607 -> 523[label="",style="solid", color="burlywood", weight=3];
489[label="merge0 vz44 compare vz45 vz46 vz47 LT\n  Ord a",fontsize=16,color="black",shape="box"];489 -> 524[label="",style="solid", color="black", weight=3];
490[label="merge0 vz44 compare vz45 vz46 vz47 EQ\n  Ord a",fontsize=16,color="black",shape="box"];490 -> 525[label="",style="solid", color="black", weight=3];
491[label="merge0 vz44 compare vz45 vz46 vz47 GT\n  Ord a",fontsize=16,color="black",shape="box"];491 -> 526[label="",style="solid", color="black", weight=3];
433[label="merge_pairs compare vz3511\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];608[label="vz3511/vz35110 : vz35111",fontsize=10,color="white",style="solid",shape="box"];433 -> 608[label="",style="solid", color="burlywood", weight=9];
608 -> 438[label="",style="solid", color="burlywood", weight=3];
609[label="vz3511/[]",fontsize=10,color="white",style="solid",shape="box"];433 -> 609[label="",style="solid", color="burlywood", weight=9];
609 -> 439[label="",style="solid", color="burlywood", weight=3];
434[label="merge compare vz34 (merge compare vz350 vz3510)\n  Ord a",fontsize=16,color="burlywood",shape="box"];610[label="vz3510/vz35100 : vz35101",fontsize=10,color="white",style="solid",shape="box"];434 -> 610[label="",style="solid", color="burlywood", weight=9];
610 -> 440[label="",style="solid", color="burlywood", weight=3];
611[label="vz3510/[]",fontsize=10,color="white",style="solid",shape="box"];434 -> 611[label="",style="solid", color="burlywood", weight=9];
611 -> 441[label="",style="solid", color="burlywood", weight=3];
435[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];436[label="merge compare vz34 vz350\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];612[label="vz350/vz3500 : vz3501",fontsize=10,color="white",style="solid",shape="box"];436 -> 612[label="",style="solid", color="burlywood", weight=9];
612 -> 442[label="",style="solid", color="burlywood", weight=3];
613[label="vz350/[]",fontsize=10,color="white",style="solid",shape="box"];436 -> 613[label="",style="solid", color="burlywood", weight=9];
613 -> 443[label="",style="solid", color="burlywood", weight=3];
523[label="compare () ()",fontsize=16,color="black",shape="box"];523 -> 570[label="",style="solid", color="black", weight=3];
524[label="vz45 : merge compare vz46 (vz44 : vz47)\n  Ord a",fontsize=16,color="green",shape="box"];524 -> 571[label="",style="dashed", color="green", weight=3];
525[label="vz45 : merge compare vz46 (vz44 : vz47)\n  Ord a",fontsize=16,color="green",shape="box"];525 -> 572[label="",style="dashed", color="green", weight=3];
526[label="vz44 : merge compare (vz45 : vz46) vz47\n  Ord a",fontsize=16,color="green",shape="box"];526 -> 573[label="",style="dashed", color="green", weight=3];
438[label="merge_pairs compare (vz35110 : vz35111)\n  Ord a",fontsize=16,color="burlywood",shape="box"];614[label="vz35111/vz351110 : vz351111",fontsize=10,color="white",style="solid",shape="box"];438 -> 614[label="",style="solid", color="burlywood", weight=9];
614 -> 445[label="",style="solid", color="burlywood", weight=3];
615[label="vz35111/[]",fontsize=10,color="white",style="solid",shape="box"];438 -> 615[label="",style="solid", color="burlywood", weight=9];
615 -> 446[label="",style="solid", color="burlywood", weight=3];
439[label="merge_pairs compare []\n  Ord a",fontsize=16,color="black",shape="box"];439 -> 447[label="",style="solid", color="black", weight=3];
440[label="merge compare vz34 (merge compare vz350 (vz35100 : vz35101))\n  Ord a",fontsize=16,color="burlywood",shape="box"];616[label="vz350/vz3500 : vz3501",fontsize=10,color="white",style="solid",shape="box"];440 -> 616[label="",style="solid", color="burlywood", weight=9];
616 -> 448[label="",style="solid", color="burlywood", weight=3];
617[label="vz350/[]",fontsize=10,color="white",style="solid",shape="box"];440 -> 617[label="",style="solid", color="burlywood", weight=9];
617 -> 449[label="",style="solid", color="burlywood", weight=3];
441[label="merge compare vz34 (merge compare vz350 [])\n  Ord a",fontsize=16,color="black",shape="box"];441 -> 450[label="",style="solid", color="black", weight=3];
442[label="merge compare vz34 (vz3500 : vz3501)\n  Ord a",fontsize=16,color="burlywood",shape="box"];618[label="vz34/vz340 : vz341",fontsize=10,color="white",style="solid",shape="box"];442 -> 618[label="",style="solid", color="burlywood", weight=9];
618 -> 451[label="",style="solid", color="burlywood", weight=3];
619[label="vz34/[]",fontsize=10,color="white",style="solid",shape="box"];442 -> 619[label="",style="solid", color="burlywood", weight=9];
619 -> 452[label="",style="solid", color="burlywood", weight=3];
443[label="merge compare vz34 []\n  Ord a",fontsize=16,color="black",shape="box"];443 -> 453[label="",style="solid", color="black", weight=3];
570[label="EQ",fontsize=16,color="green",shape="box"];571 -> 436[label="",style="dashed", color="red", weight=0];
571[label="merge compare vz46 (vz44 : vz47)\n  Ord a",fontsize=16,color="magenta"];571 -> 574[label="",style="dashed", color="magenta", weight=3];
571 -> 575[label="",style="dashed", color="magenta", weight=3];
572 -> 436[label="",style="dashed", color="red", weight=0];
572[label="merge compare vz46 (vz44 : vz47)\n  Ord a",fontsize=16,color="magenta"];572 -> 576[label="",style="dashed", color="magenta", weight=3];
572 -> 577[label="",style="dashed", color="magenta", weight=3];
573 -> 436[label="",style="dashed", color="red", weight=0];
573[label="merge compare (vz45 : vz46) vz47\n  Ord a",fontsize=16,color="magenta"];573 -> 578[label="",style="dashed", color="magenta", weight=3];
573 -> 579[label="",style="dashed", color="magenta", weight=3];
445[label="merge_pairs compare (vz35110 : vz351110 : vz351111)\n  Ord a",fontsize=16,color="black",shape="box"];445 -> 455[label="",style="solid", color="black", weight=3];
446[label="merge_pairs compare (vz35110 : [])\n  Ord a",fontsize=16,color="black",shape="box"];446 -> 456[label="",style="solid", color="black", weight=3];
447[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];448[label="merge compare vz34 (merge compare (vz3500 : vz3501) (vz35100 : vz35101))\n  Ord a",fontsize=16,color="black",shape="box"];448 -> 457[label="",style="solid", color="black", weight=3];
449[label="merge compare vz34 (merge compare [] (vz35100 : vz35101))\n  Ord a",fontsize=16,color="black",shape="box"];449 -> 458[label="",style="solid", color="black", weight=3];
450 -> 436[label="",style="dashed", color="red", weight=0];
450[label="merge compare vz34 vz350\n  Ord a",fontsize=16,color="magenta"];451[label="merge compare (vz340 : vz341) (vz3500 : vz3501)\n  Ord a",fontsize=16,color="black",shape="box"];451 -> 459[label="",style="solid", color="black", weight=3];
452[label="merge compare [] (vz3500 : vz3501)\n  Ord a",fontsize=16,color="black",shape="box"];452 -> 460[label="",style="solid", color="black", weight=3];
453[label="vz34\n  Ord a",fontsize=16,color="green",shape="box"];574[label="vz46\n  Ord a",fontsize=16,color="green",shape="box"];575[label="vz44 : vz47\n  Ord a",fontsize=16,color="green",shape="box"];576[label="vz46\n  Ord a",fontsize=16,color="green",shape="box"];577[label="vz44 : vz47\n  Ord a",fontsize=16,color="green",shape="box"];578[label="vz45 : vz46\n  Ord a",fontsize=16,color="green",shape="box"];579[label="vz47\n  Ord a",fontsize=16,color="green",shape="box"];455[label="merge compare vz35110 vz351110 : merge_pairs compare vz351111\n  Ord a",fontsize=16,color="green",shape="box"];455 -> 463[label="",style="dashed", color="green", weight=3];
455 -> 464[label="",style="dashed", color="green", weight=3];
456[label="vz35110 : []\n  Ord a",fontsize=16,color="green",shape="box"];457 -> 436[label="",style="dashed", color="red", weight=0];
457[label="merge compare vz34 (merge0 vz35100 compare vz3500 vz3501 vz35101 (compare vz3500 vz35100))\n  Ord a",fontsize=16,color="magenta"];457 -> 465[label="",style="dashed", color="magenta", weight=3];
458 -> 436[label="",style="dashed", color="red", weight=0];
458[label="merge compare vz34 (vz35100 : vz35101)\n  Ord a",fontsize=16,color="magenta"];458 -> 466[label="",style="dashed", color="magenta", weight=3];
459 -> 467[label="",style="dashed", color="red", weight=0];
459[label="merge0 vz3500 compare vz340 vz341 vz3501 (compare vz340 vz3500)\n  Ord a",fontsize=16,color="magenta"];459 -> 478[label="",style="dashed", color="magenta", weight=3];
459 -> 479[label="",style="dashed", color="magenta", weight=3];
459 -> 480[label="",style="dashed", color="magenta", weight=3];
459 -> 481[label="",style="dashed", color="magenta", weight=3];
459 -> 482[label="",style="dashed", color="magenta", weight=3];
460[label="vz3500 : vz3501\n  Ord a",fontsize=16,color="green",shape="box"];463 -> 436[label="",style="dashed", color="red", weight=0];
463[label="merge compare vz35110 vz351110\n  Ord a",fontsize=16,color="magenta"];463 -> 492[label="",style="dashed", color="magenta", weight=3];
463 -> 493[label="",style="dashed", color="magenta", weight=3];
464 -> 433[label="",style="dashed", color="red", weight=0];
464[label="merge_pairs compare vz351111\n  Ord a",fontsize=16,color="magenta"];464 -> 494[label="",style="dashed", color="magenta", weight=3];
465 -> 467[label="",style="dashed", color="red", weight=0];
465[label="merge0 vz35100 compare vz3500 vz3501 vz35101 (compare vz3500 vz35100)\n  Ord a",fontsize=16,color="magenta"];465 -> 483[label="",style="dashed", color="magenta", weight=3];
465 -> 484[label="",style="dashed", color="magenta", weight=3];
465 -> 485[label="",style="dashed", color="magenta", weight=3];
465 -> 486[label="",style="dashed", color="magenta", weight=3];
465 -> 487[label="",style="dashed", color="magenta", weight=3];
466[label="vz35100 : vz35101\n  Ord a",fontsize=16,color="green",shape="box"];478[label="vz3501\n  Ord a",fontsize=16,color="green",shape="box"];479[label="compare vz340 vz3500\n  Ord a",fontsize=16,color="blue",shape="box"];630[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 630[label="",style="solid", color="blue", weight=9];
630 -> 495[label="",style="solid", color="blue", weight=3];
631[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 631[label="",style="solid", color="blue", weight=9];
631 -> 496[label="",style="solid", color="blue", weight=3];
632[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 632[label="",style="solid", color="blue", weight=9];
632 -> 497[label="",style="solid", color="blue", weight=3];
633[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 633[label="",style="solid", color="blue", weight=9];
633 -> 498[label="",style="solid", color="blue", weight=3];
634[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 634[label="",style="solid", color="blue", weight=9];
634 -> 499[label="",style="solid", color="blue", weight=3];
635[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 635[label="",style="solid", color="blue", weight=9];
635 -> 500[label="",style="solid", color="blue", weight=3];
636[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 636[label="",style="solid", color="blue", weight=9];
636 -> 501[label="",style="solid", color="blue", weight=3];
637[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 637[label="",style="solid", color="blue", weight=9];
637 -> 502[label="",style="solid", color="blue", weight=3];
638[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 638[label="",style="solid", color="blue", weight=9];
638 -> 503[label="",style="solid", color="blue", weight=3];
639[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 639[label="",style="solid", color="blue", weight=9];
639 -> 504[label="",style="solid", color="blue", weight=3];
640[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 640[label="",style="solid", color="blue", weight=9];
640 -> 505[label="",style="solid", color="blue", weight=3];
641[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 641[label="",style="solid", color="blue", weight=9];
641 -> 506[label="",style="solid", color="blue", weight=3];
642[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 642[label="",style="solid", color="blue", weight=9];
642 -> 507[label="",style="solid", color="blue", weight=3];
643[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];479 -> 643[label="",style="solid", color="blue", weight=9];
643 -> 508[label="",style="solid", color="blue", weight=3];
480[label="vz341\n  Ord a",fontsize=16,color="green",shape="box"];481[label="vz340\n  Ord a",fontsize=16,color="green",shape="box"];482[label="vz3500\n  Ord a",fontsize=16,color="green",shape="box"];492[label="vz35110\n  Ord a",fontsize=16,color="green",shape="box"];493[label="vz351110\n  Ord a",fontsize=16,color="green",shape="box"];494[label="vz351111\n  Ord a",fontsize=16,color="green",shape="box"];483[label="vz35101\n  Ord a",fontsize=16,color="green",shape="box"];484[label="compare vz3500 vz35100\n  Ord a",fontsize=16,color="blue",shape="box"];644[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 644[label="",style="solid", color="blue", weight=9];
644 -> 509[label="",style="solid", color="blue", weight=3];
645[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 645[label="",style="solid", color="blue", weight=9];
645 -> 510[label="",style="solid", color="blue", weight=3];
646[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 646[label="",style="solid", color="blue", weight=9];
646 -> 511[label="",style="solid", color="blue", weight=3];
647[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 647[label="",style="solid", color="blue", weight=9];
647 -> 512[label="",style="solid", color="blue", weight=3];
648[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 648[label="",style="solid", color="blue", weight=9];
648 -> 513[label="",style="solid", color="blue", weight=3];
649[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 649[label="",style="solid", color="blue", weight=9];
649 -> 514[label="",style="solid", color="blue", weight=3];
650[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 650[label="",style="solid", color="blue", weight=9];
650 -> 515[label="",style="solid", color="blue", weight=3];
651[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 651[label="",style="solid", color="blue", weight=9];
651 -> 516[label="",style="solid", color="blue", weight=3];
652[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 652[label="",style="solid", color="blue", weight=9];
652 -> 517[label="",style="solid", color="blue", weight=3];
653[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 653[label="",style="solid", color="blue", weight=9];
653 -> 518[label="",style="solid", color="blue", weight=3];
654[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 654[label="",style="solid", color="blue", weight=9];
654 -> 519[label="",style="solid", color="blue", weight=3];
655[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 655[label="",style="solid", color="blue", weight=9];
655 -> 520[label="",style="solid", color="blue", weight=3];
656[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 656[label="",style="solid", color="blue", weight=9];
656 -> 521[label="",style="solid", color="blue", weight=3];
657[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];484 -> 657[label="",style="solid", color="blue", weight=9];
657 -> 522[label="",style="solid", color="blue", weight=3];
485[label="vz3501\n  Ord a",fontsize=16,color="green",shape="box"];486[label="vz3500\n  Ord a",fontsize=16,color="green",shape="box"];487[label="vz35100\n  Ord a",fontsize=16,color="green",shape="box"];495[label="compare vz340 vz3500\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];495 -> 527[label="",style="solid", color="black", weight=3];
496[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];496 -> 528[label="",style="solid", color="black", weight=3];
497[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];497 -> 529[label="",style="solid", color="black", weight=3];
498[label="compare vz340 vz3500\n  Ord a",fontsize=16,color="black",shape="triangle"];498 -> 530[label="",style="solid", color="black", weight=3];
499[label="compare vz340 vz3500\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];499 -> 531[label="",style="solid", color="black", weight=3];
500 -> 469[label="",style="dashed", color="red", weight=0];
500[label="compare vz340 vz3500",fontsize=16,color="magenta"];500 -> 532[label="",style="dashed", color="magenta", weight=3];
500 -> 533[label="",style="dashed", color="magenta", weight=3];
501[label="compare vz340 vz3500\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="triangle"];501 -> 534[label="",style="solid", color="black", weight=3];
502[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];502 -> 535[label="",style="solid", color="black", weight=3];
503[label="compare vz340 vz3500\n  Ord a",fontsize=16,color="black",shape="triangle"];503 -> 536[label="",style="solid", color="black", weight=3];
504[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];504 -> 537[label="",style="solid", color="black", weight=3];
505[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];505 -> 538[label="",style="solid", color="black", weight=3];
506[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];506 -> 539[label="",style="solid", color="black", weight=3];
507[label="compare vz340 vz3500\n  Integral a",fontsize=16,color="black",shape="triangle"];507 -> 540[label="",style="solid", color="black", weight=3];
508[label="compare vz340 vz3500",fontsize=16,color="black",shape="triangle"];508 -> 541[label="",style="solid", color="black", weight=3];
509 -> 495[label="",style="dashed", color="red", weight=0];
509[label="compare vz3500 vz35100\n  Ord a  Ord b",fontsize=16,color="magenta"];509 -> 542[label="",style="dashed", color="magenta", weight=3];
509 -> 543[label="",style="dashed", color="magenta", weight=3];
510 -> 496[label="",style="dashed", color="red", weight=0];
510[label="compare vz3500 vz35100",fontsize=16,color="magenta"];510 -> 544[label="",style="dashed", color="magenta", weight=3];
510 -> 545[label="",style="dashed", color="magenta", weight=3];
511 -> 497[label="",style="dashed", color="red", weight=0];
511[label="compare vz3500 vz35100",fontsize=16,color="magenta"];511 -> 546[label="",style="dashed", color="magenta", weight=3];
511 -> 547[label="",style="dashed", color="magenta", weight=3];
512 -> 498[label="",style="dashed", color="red", weight=0];
512[label="compare vz3500 vz35100\n  Ord a",fontsize=16,color="magenta"];512 -> 548[label="",style="dashed", color="magenta", weight=3];
512 -> 549[label="",style="dashed", color="magenta", weight=3];
513 -> 499[label="",style="dashed", color="red", weight=0];
513[label="compare vz3500 vz35100\n  Ord a  Ord b",fontsize=16,color="magenta"];513 -> 550[label="",style="dashed", color="magenta", weight=3];
513 -> 551[label="",style="dashed", color="magenta", weight=3];
514 -> 469[label="",style="dashed", color="red", weight=0];
514[label="compare vz3500 vz35100",fontsize=16,color="magenta"];514 -> 552[label="",style="dashed", color="magenta", weight=3];
514 -> 553[label="",style="dashed", color="magenta", weight=3];
515 -> 501[label="",style="dashed", color="red", weight=0];
515[label="compare vz3500 vz35100\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];515 -> 554[label="",style="dashed", color="magenta", weight=3];
515 -> 555[label="",style="dashed", color="magenta", weight=3];
516 -> 502[label="",style="dashed", color="red", weight=0];
516[label="compare vz3500 vz35100",fontsize=16,color="magenta"];516 -> 556[label="",style="dashed", color="magenta", weight=3];
516 -> 557[label="",style="dashed", color="magenta", weight=3];
517 -> 503[label="",style="dashed", color="red", weight=0];
517[label="compare vz3500 vz35100\n  Ord a",fontsize=16,color="magenta"];517 -> 558[label="",style="dashed", color="magenta", weight=3];
517 -> 559[label="",style="dashed", color="magenta", weight=3];
518 -> 504[label="",style="dashed", color="red", weight=0];
518[label="compare vz3500 vz35100",fontsize=16,color="magenta"];518 -> 560[label="",style="dashed", color="magenta", weight=3];
518 -> 561[label="",style="dashed", color="magenta", weight=3];
519 -> 505[label="",style="dashed", color="red", weight=0];
519[label="compare vz3500 vz35100",fontsize=16,color="magenta"];519 -> 562[label="",style="dashed", color="magenta", weight=3];
519 -> 563[label="",style="dashed", color="magenta", weight=3];
520 -> 506[label="",style="dashed", color="red", weight=0];
520[label="compare vz3500 vz35100",fontsize=16,color="magenta"];520 -> 564[label="",style="dashed", color="magenta", weight=3];
520 -> 565[label="",style="dashed", color="magenta", weight=3];
521 -> 507[label="",style="dashed", color="red", weight=0];
521[label="compare vz3500 vz35100\n  Integral a",fontsize=16,color="magenta"];521 -> 566[label="",style="dashed", color="magenta", weight=3];
521 -> 567[label="",style="dashed", color="magenta", weight=3];
522 -> 508[label="",style="dashed", color="red", weight=0];
522[label="compare vz3500 vz35100",fontsize=16,color="magenta"];522 -> 568[label="",style="dashed", color="magenta", weight=3];
522 -> 569[label="",style="dashed", color="magenta", weight=3];
527[label="error []",fontsize=16,color="red",shape="box"];528[label="error []",fontsize=16,color="red",shape="box"];529[label="error []",fontsize=16,color="red",shape="box"];530[label="error []",fontsize=16,color="red",shape="box"];531[label="error []",fontsize=16,color="red",shape="box"];532[label="vz340",fontsize=16,color="green",shape="box"];533[label="vz3500",fontsize=16,color="green",shape="box"];534[label="error []",fontsize=16,color="red",shape="box"];535[label="error []",fontsize=16,color="red",shape="box"];536[label="error []",fontsize=16,color="red",shape="box"];537[label="error []",fontsize=16,color="red",shape="box"];538[label="error []",fontsize=16,color="red",shape="box"];539[label="error []",fontsize=16,color="red",shape="box"];540[label="error []",fontsize=16,color="red",shape="box"];541[label="error []",fontsize=16,color="red",shape="box"];542[label="vz35100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];543[label="vz3500\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];544[label="vz35100",fontsize=16,color="green",shape="box"];545[label="vz3500",fontsize=16,color="green",shape="box"];546[label="vz35100",fontsize=16,color="green",shape="box"];547[label="vz3500",fontsize=16,color="green",shape="box"];548[label="vz35100\n  Ord a",fontsize=16,color="green",shape="box"];549[label="vz3500\n  Ord a",fontsize=16,color="green",shape="box"];550[label="vz35100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];551[label="vz3500\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];552[label="vz3500",fontsize=16,color="green",shape="box"];553[label="vz35100",fontsize=16,color="green",shape="box"];554[label="vz35100\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];555[label="vz3500\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];556[label="vz35100",fontsize=16,color="green",shape="box"];557[label="vz3500",fontsize=16,color="green",shape="box"];558[label="vz35100\n  Ord a",fontsize=16,color="green",shape="box"];559[label="vz3500\n  Ord a",fontsize=16,color="green",shape="box"];560[label="vz35100",fontsize=16,color="green",shape="box"];561[label="vz3500",fontsize=16,color="green",shape="box"];562[label="vz35100",fontsize=16,color="green",shape="box"];563[label="vz3500",fontsize=16,color="green",shape="box"];564[label="vz35100",fontsize=16,color="green",shape="box"];565[label="vz3500",fontsize=16,color="green",shape="box"];566[label="vz35100\n  Integral a",fontsize=16,color="green",shape="box"];567[label="vz3500\n  Integral a",fontsize=16,color="green",shape="box"];568[label="vz35100",fontsize=16,color="green",shape="box"];569[label="vz3500",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_map(:(vz3110, vz3111)) → new_map(vz3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_map(:(vz3110, vz3111)) → new_map(vz3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz44, vz45, vz46, vz47, GT, ba) → new_merge(:(vz45, vz46), vz47, ba)
new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(vz340, vz341), :(vz3500, vz3501), bb) → new_merge0(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, bb), bb)
new_merge0(vz44, vz45, vz46, vz47, LT, ba) → new_merge(vz46, :(vz44, vz47), ba)

The TRS R consists of the following rules:

new_compare2(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, app(ty_Ratio, bc)) → new_compare2(vz340, vz3500, bc)
new_compare4(vz340, vz3500) → error([])
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bf)) → new_compare9(vz340, vz3500, bf)
new_compare(vz340, vz3500, ty_Integer) → new_compare4(vz340, vz3500)
new_compare7(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare5(vz340, vz3500)
new_compare(vz340, vz3500, ty_Double) → new_compare1(vz340, vz3500)
new_compare13(vz340, vz3500, cd) → error([])
new_compare11(@0, @0) → EQ
new_compare(vz340, vz3500, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz340, vz3500, ca, cb, cc)
new_compare1(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Bool) → new_compare3(vz340, vz3500)
new_compare(vz340, vz3500, ty_@0) → new_compare11(vz340, vz3500)
new_compare6(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Float) → new_compare7(vz340, vz3500)
new_compare5(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(app(ty_Either, bg), bh)) → new_compare10(vz340, vz3500, bg, bh)
new_compare8(vz340, vz3500, bd, be) → error([])
new_compare12(vz340, vz3500, ca, cb, cc) → error([])
new_compare9(vz340, vz3500, bf) → error([])
new_compare(vz340, vz3500, app(app(ty_@2, bd), be)) → new_compare8(vz340, vz3500, bd, be)
new_compare(vz340, vz3500, app(ty_[], cd)) → new_compare13(vz340, vz3500, cd)
new_compare(vz340, vz3500, ty_Char) → new_compare0(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, bg, bh) → error([])
new_compare(vz340, vz3500, ty_Ordering) → new_compare6(vz340, vz3500)

The set Q consists of the following terms:

new_compare12(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare3(x0, x1)
new_compare2(x0, x1, x2)
new_compare9(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare11(@0, @0)
new_compare5(x0, x1)
new_compare8(x0, x1, x2, x3)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_Bool)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare13(x0, x1, x2)
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Integer)
new_compare(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
new_merge(:(vz340, vz341), :(vz3500, vz3501), bb) → new_merge0(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, bb), bb)

The TRS R consists of the following rules:

new_compare2(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, app(ty_Ratio, bc)) → new_compare2(vz340, vz3500, bc)
new_compare4(vz340, vz3500) → error([])
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bf)) → new_compare9(vz340, vz3500, bf)
new_compare(vz340, vz3500, ty_Integer) → new_compare4(vz340, vz3500)
new_compare7(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Int) → new_compare5(vz340, vz3500)
new_compare(vz340, vz3500, ty_Double) → new_compare1(vz340, vz3500)
new_compare13(vz340, vz3500, cd) → error([])
new_compare11(@0, @0) → EQ
new_compare(vz340, vz3500, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz340, vz3500, ca, cb, cc)
new_compare1(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Bool) → new_compare3(vz340, vz3500)
new_compare(vz340, vz3500, ty_@0) → new_compare11(vz340, vz3500)
new_compare6(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_Float) → new_compare7(vz340, vz3500)
new_compare5(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(app(ty_Either, bg), bh)) → new_compare10(vz340, vz3500, bg, bh)
new_compare8(vz340, vz3500, bd, be) → error([])
new_compare12(vz340, vz3500, ca, cb, cc) → error([])
new_compare9(vz340, vz3500, bf) → error([])
new_compare(vz340, vz3500, app(app(ty_@2, bd), be)) → new_compare8(vz340, vz3500, bd, be)
new_compare(vz340, vz3500, app(ty_[], cd)) → new_compare13(vz340, vz3500, cd)
new_compare(vz340, vz3500, ty_Char) → new_compare0(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, bg, bh) → error([])
new_compare(vz340, vz3500, ty_Ordering) → new_compare6(vz340, vz3500)

The set Q consists of the following terms:

new_compare12(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare3(x0, x1)
new_compare2(x0, x1, x2)
new_compare9(x0, x1, x2)
new_compare(x0, x1, ty_Int)
new_compare7(x0, x1)
new_compare4(x0, x1)
new_compare0(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare11(@0, @0)
new_compare5(x0, x1)
new_compare8(x0, x1, x2, x3)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, x2, x3)
new_compare(x0, x1, ty_Bool)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare13(x0, x1, x2)
new_compare(x0, x1, ty_Ordering)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, ty_Integer)
new_compare(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_merge0(vz44, vz45, vz46, vz47, EQ, ba) → new_merge(vz46, :(vz44, vz47), ba)
The graph contains the following edges 3 >= 1, 6 >= 3
new_merge(:(vz340, vz341), :(vz3500, vz3501), bb) → new_merge0(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, bb), bb)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge_pairs(:(vz35110, :(vz351110, vz351111)), ba) → new_merge_pairs(vz351111, ba)

From the DPs we obtained the following set of size-change graphs:

new_merge_pairs(:(vz35110, :(vz351110, vz351111)), ba) → new_merge_pairs(vz351111, ba)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz34, :(vz350, []), ba) → new_mergesort'(new_merge2(vz34, vz350, ba), [], ba)
new_mergesort'(vz34, :(vz350, :(vz3510, vz3511)), ba) → new_mergesort'(new_merge1(vz34, vz350, vz3510, ba), new_merge_pairs0(vz3511, ba), ba)

The TRS R consists of the following rules:

new_compare14(vz3500, vz35100, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz3500, vz35100, ca, cb, cc)
new_compare2(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, app(ty_Ratio, bc)) → new_compare2(vz340, vz3500, bc)
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bf)) → new_compare9(vz340, vz3500, bf)
new_merge00(vz44, vz45, vz46, vz47, LT, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare14(vz3500, vz35100, app(app(ty_@2, bd), be)) → new_compare8(vz3500, vz35100, bd, be)
new_compare7(vz340, vz3500) → error([])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
new_compare(vz340, vz3500, ty_Double) → new_compare1(vz340, vz3500)
new_compare13(vz340, vz3500, cd) → error([])
new_merge1(vz34, [], :(vz35100, vz35101), ba) → new_merge2(vz34, :(vz35100, vz35101), ba)
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_compare(vz340, vz3500, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz340, vz3500, ca, cb, cc)
new_compare(vz340, vz3500, ty_Bool) → new_compare3(vz340, vz3500)
new_merge1(vz34, :(vz3500, vz3501), :(vz35100, vz35101), ba) → new_merge2(vz34, new_merge00(vz35100, vz3500, vz3501, vz35101, new_compare14(vz3500, vz35100, ba), ba), ba)
new_compare14(vz3500, vz35100, ty_Ordering) → new_compare6(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Bool) → new_compare3(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(ty_Either, bg), bh)) → new_compare10(vz340, vz3500, bg, bh)
new_compare8(vz340, vz3500, bd, be) → error([])
new_merge00(vz44, vz45, vz46, vz47, GT, bb) → :(vz44, new_merge2(:(vz45, vz46), vz47, bb))
new_compare(vz340, vz3500, app(app(ty_@2, bd), be)) → new_compare8(vz340, vz3500, bd, be)
new_compare(vz340, vz3500, ty_Char) → new_compare0(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, bg, bh) → error([])
new_merge2([], :(vz3500, vz3501), ba) → :(vz3500, vz3501)
new_compare(vz340, vz3500, ty_Ordering) → new_compare6(vz340, vz3500)
new_merge_pairs0([], ba) → []
new_compare14(vz3500, vz35100, ty_Char) → new_compare0(vz3500, vz35100)
new_compare4(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, ty_Double) → new_compare1(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Float) → new_compare7(vz3500, vz35100)
new_compare14(vz3500, vz35100, app(ty_[], cd)) → new_compare13(vz3500, vz35100, cd)
new_compare(vz340, vz3500, ty_Integer) → new_compare4(vz340, vz3500)
new_merge1(vz34, vz350, [], ba) → new_merge2(vz34, vz350, ba)
new_compare14(vz3500, vz35100, app(ty_Maybe, bf)) → new_compare9(vz3500, vz35100, bf)
new_merge2(:(vz340, vz341), :(vz3500, vz3501), ba) → new_merge00(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, ba), ba)
new_compare(vz340, vz3500, ty_Int) → new_compare5(vz340, vz3500)
new_compare14(vz3500, vz35100, app(app(ty_Either, bg), bh)) → new_compare10(vz3500, vz35100, bg, bh)
new_compare14(vz3500, vz35100, ty_Int) → new_compare5(vz3500, vz35100)
new_compare11(@0, @0) → EQ
new_merge2(vz34, [], ba) → vz34
new_compare1(vz340, vz3500) → error([])
new_compare6(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_@0) → new_compare11(vz340, vz3500)
new_compare(vz340, vz3500, ty_Float) → new_compare7(vz340, vz3500)
new_compare5(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, ty_@0) → new_compare11(vz3500, vz35100)
new_compare12(vz340, vz3500, ca, cb, cc) → error([])
new_compare9(vz340, vz3500, bf) → error([])
new_compare(vz340, vz3500, app(ty_[], cd)) → new_compare13(vz340, vz3500, cd)
new_compare14(vz3500, vz35100, app(ty_Ratio, bc)) → new_compare2(vz3500, vz35100, bc)
new_merge00(vz44, vz45, vz46, vz47, EQ, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare14(vz3500, vz35100, ty_Integer) → new_compare4(vz3500, vz35100)

The set Q consists of the following terms:

new_compare3(x0, x1)
new_compare2(x0, x1, x2)
new_compare9(x0, x1, x2)
new_compare7(x0, x1)
new_compare(x0, x1, ty_Int)
new_compare4(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare5(x0, x1)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_Bool)
new_compare1(x0, x1)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge2([], :(x0, x1), x2)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare(x0, x1, ty_Float)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, ty_Ordering)
new_compare14(x0, x1, ty_Bool)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_merge00(x0, x1, x2, x3, EQ, x4)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, ty_@0)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, app(ty_Ratio, x2))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, ty_@0)
new_compare12(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_merge_pairs0([], x0)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, ty_Char)
new_compare14(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, ty_Ordering)
new_compare0(x0, x1)
new_compare11(@0, @0)
new_compare8(x0, x1, x2, x3)
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, x2, x3)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare14(x0, x1, ty_Integer)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Int)
new_compare13(x0, x1, x2)
new_compare14(x0, x1, ty_Float)
new_merge_pairs0(:(x0, []), x1)
new_merge1(x0, [], :(x1, x2), x3)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, ty_Double)
new_compare(x0, x1, ty_Integer)
new_merge2(x0, [], x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz34, :(vz350, :(vz3510, vz3511)), ba) → new_mergesort'(new_merge1(vz34, vz350, vz3510, ba), new_merge_pairs0(vz3511, ba), ba)

The TRS R consists of the following rules:

new_compare14(vz3500, vz35100, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz3500, vz35100, ca, cb, cc)
new_compare2(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, app(ty_Ratio, bc)) → new_compare2(vz340, vz3500, bc)
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bf)) → new_compare9(vz340, vz3500, bf)
new_merge00(vz44, vz45, vz46, vz47, LT, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare14(vz3500, vz35100, app(app(ty_@2, bd), be)) → new_compare8(vz3500, vz35100, bd, be)
new_compare7(vz340, vz3500) → error([])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
new_compare(vz340, vz3500, ty_Double) → new_compare1(vz340, vz3500)
new_compare13(vz340, vz3500, cd) → error([])
new_merge1(vz34, [], :(vz35100, vz35101), ba) → new_merge2(vz34, :(vz35100, vz35101), ba)
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_compare(vz340, vz3500, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz340, vz3500, ca, cb, cc)
new_compare(vz340, vz3500, ty_Bool) → new_compare3(vz340, vz3500)
new_merge1(vz34, :(vz3500, vz3501), :(vz35100, vz35101), ba) → new_merge2(vz34, new_merge00(vz35100, vz3500, vz3501, vz35101, new_compare14(vz3500, vz35100, ba), ba), ba)
new_compare14(vz3500, vz35100, ty_Ordering) → new_compare6(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Bool) → new_compare3(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(ty_Either, bg), bh)) → new_compare10(vz340, vz3500, bg, bh)
new_compare8(vz340, vz3500, bd, be) → error([])
new_merge00(vz44, vz45, vz46, vz47, GT, bb) → :(vz44, new_merge2(:(vz45, vz46), vz47, bb))
new_compare(vz340, vz3500, app(app(ty_@2, bd), be)) → new_compare8(vz340, vz3500, bd, be)
new_compare(vz340, vz3500, ty_Char) → new_compare0(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, bg, bh) → error([])
new_merge2([], :(vz3500, vz3501), ba) → :(vz3500, vz3501)
new_compare(vz340, vz3500, ty_Ordering) → new_compare6(vz340, vz3500)
new_merge_pairs0([], ba) → []
new_compare14(vz3500, vz35100, ty_Char) → new_compare0(vz3500, vz35100)
new_compare4(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, ty_Double) → new_compare1(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Float) → new_compare7(vz3500, vz35100)
new_compare14(vz3500, vz35100, app(ty_[], cd)) → new_compare13(vz3500, vz35100, cd)
new_compare(vz340, vz3500, ty_Integer) → new_compare4(vz340, vz3500)
new_merge1(vz34, vz350, [], ba) → new_merge2(vz34, vz350, ba)
new_compare14(vz3500, vz35100, app(ty_Maybe, bf)) → new_compare9(vz3500, vz35100, bf)
new_merge2(:(vz340, vz341), :(vz3500, vz3501), ba) → new_merge00(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, ba), ba)
new_compare(vz340, vz3500, ty_Int) → new_compare5(vz340, vz3500)
new_compare14(vz3500, vz35100, app(app(ty_Either, bg), bh)) → new_compare10(vz3500, vz35100, bg, bh)
new_compare14(vz3500, vz35100, ty_Int) → new_compare5(vz3500, vz35100)
new_compare11(@0, @0) → EQ
new_merge2(vz34, [], ba) → vz34
new_compare1(vz340, vz3500) → error([])
new_compare6(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_@0) → new_compare11(vz340, vz3500)
new_compare(vz340, vz3500, ty_Float) → new_compare7(vz340, vz3500)
new_compare5(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, ty_@0) → new_compare11(vz3500, vz35100)
new_compare12(vz340, vz3500, ca, cb, cc) → error([])
new_compare9(vz340, vz3500, bf) → error([])
new_compare(vz340, vz3500, app(ty_[], cd)) → new_compare13(vz340, vz3500, cd)
new_compare14(vz3500, vz35100, app(ty_Ratio, bc)) → new_compare2(vz3500, vz35100, bc)
new_merge00(vz44, vz45, vz46, vz47, EQ, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare14(vz3500, vz35100, ty_Integer) → new_compare4(vz3500, vz35100)

The set Q consists of the following terms:

new_compare3(x0, x1)
new_compare2(x0, x1, x2)
new_compare9(x0, x1, x2)
new_compare7(x0, x1)
new_compare(x0, x1, ty_Int)
new_compare4(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare5(x0, x1)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_Bool)
new_compare1(x0, x1)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge2([], :(x0, x1), x2)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare(x0, x1, ty_Float)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, ty_Ordering)
new_compare14(x0, x1, ty_Bool)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_merge00(x0, x1, x2, x3, EQ, x4)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, ty_@0)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, app(ty_Ratio, x2))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, ty_@0)
new_compare12(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_merge_pairs0([], x0)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, ty_Char)
new_compare14(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, ty_Ordering)
new_compare0(x0, x1)
new_compare11(@0, @0)
new_compare8(x0, x1, x2, x3)
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, x2, x3)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare14(x0, x1, ty_Integer)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Int)
new_compare13(x0, x1, x2)
new_compare14(x0, x1, ty_Float)
new_merge_pairs0(:(x0, []), x1)
new_merge1(x0, [], :(x1, x2), x3)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, ty_Double)
new_compare(x0, x1, ty_Integer)
new_merge2(x0, [], x1)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_mergesort'(vz34, :(vz350, :(vz3510, vz3511)), ba) → new_mergesort'(new_merge1(vz34, vz350, vz3510, ba), new_merge_pairs0(vz3511, ba), ba)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(@0) = 0
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL([]) = 0
POL(app(x₁, x₂)) = 1 + x₁ + x₂
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(new_compare0(x₁, x₂)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂, x₃, x₄)) = 1
POL(new_compare11(x₁, x₂)) = 0
POL(new_compare12(x₁, x₂, x₃, x₄, x₅)) = 1
POL(new_compare13(x₁, x₂, x₃)) = 1
POL(new_compare14(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(new_compare2(x₁, x₂, x₃)) = 1
POL(new_compare3(x₁, x₂)) = 0
POL(new_compare4(x₁, x₂)) = 1
POL(new_compare5(x₁, x₂)) = 1
POL(new_compare6(x₁, x₂)) = 1
POL(new_compare7(x₁, x₂)) = 1
POL(new_compare8(x₁, x₂, x₃, x₄)) = 1
POL(new_compare9(x₁, x₂, x₃)) = 1
POL(new_merge00(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(new_merge1(x₁, x₂, x₃, x₄)) = 0
POL(new_merge2(x₁, x₂, x₃)) = 0
POL(new_merge_pairs0(x₁, x₂)) = 1 + x₁
POL(new_mergesort'(x₁, x₂, x₃)) = x₂
POL(ty_@0) = 1
POL(ty_@2) = 0
POL(ty_@3) = 1
POL(ty_Bool) = 1
POL(ty_Char) = 1
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 1
POL(ty_Int) = 1
POL(ty_Integer) = 1
POL(ty_Maybe) = 1
POL(ty_Ordering) = 1
POL(ty_Ratio) = 1
POL(ty_[]) = 0

The following usable rules [17] were oriented:

new_merge_pairs0([], ba) → []
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_compare14(vz3500, vz35100, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz3500, vz35100, ca, cb, cc)
new_compare2(vz340, vz3500, bc) → error([])
new_compare(vz340, vz3500, app(ty_Ratio, bc)) → new_compare2(vz340, vz3500, bc)
new_compare0(vz340, vz3500) → error([])
new_compare(vz340, vz3500, app(ty_Maybe, bf)) → new_compare9(vz340, vz3500, bf)
new_merge00(vz44, vz45, vz46, vz47, LT, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare14(vz3500, vz35100, app(app(ty_@2, bd), be)) → new_compare8(vz3500, vz35100, bd, be)
new_compare7(vz340, vz3500) → error([])
new_merge_pairs0(:(vz35110, :(vz351110, vz351111)), ba) → :(new_merge2(vz35110, vz351110, ba), new_merge_pairs0(vz351111, ba))
new_compare(vz340, vz3500, ty_Double) → new_compare1(vz340, vz3500)
new_compare13(vz340, vz3500, cd) → error([])
new_merge1(vz34, [], :(vz35100, vz35101), ba) → new_merge2(vz34, :(vz35100, vz35101), ba)
new_merge_pairs0(:(vz35110, []), ba) → :(vz35110, [])
new_compare(vz340, vz3500, app(app(app(ty_@3, ca), cb), cc)) → new_compare12(vz340, vz3500, ca, cb, cc)
new_compare(vz340, vz3500, ty_Bool) → new_compare3(vz340, vz3500)
new_merge1(vz34, :(vz3500, vz3501), :(vz35100, vz35101), ba) → new_merge2(vz34, new_merge00(vz35100, vz3500, vz3501, vz35101, new_compare14(vz3500, vz35100, ba), ba), ba)
new_compare14(vz3500, vz35100, ty_Ordering) → new_compare6(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Bool) → new_compare3(vz3500, vz35100)
new_compare(vz340, vz3500, app(app(ty_Either, bg), bh)) → new_compare10(vz340, vz3500, bg, bh)
new_compare8(vz340, vz3500, bd, be) → error([])
new_merge00(vz44, vz45, vz46, vz47, GT, bb) → :(vz44, new_merge2(:(vz45, vz46), vz47, bb))
new_compare(vz340, vz3500, app(app(ty_@2, bd), be)) → new_compare8(vz340, vz3500, bd, be)
new_compare(vz340, vz3500, ty_Char) → new_compare0(vz340, vz3500)
new_compare3(vz340, vz3500) → error([])
new_compare10(vz340, vz3500, bg, bh) → error([])
new_merge2([], :(vz3500, vz3501), ba) → :(vz3500, vz3501)
new_compare(vz340, vz3500, ty_Ordering) → new_compare6(vz340, vz3500)
new_merge_pairs0([], ba) → []
new_compare14(vz3500, vz35100, ty_Char) → new_compare0(vz3500, vz35100)
new_compare4(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, ty_Double) → new_compare1(vz3500, vz35100)
new_compare14(vz3500, vz35100, ty_Float) → new_compare7(vz3500, vz35100)
new_compare14(vz3500, vz35100, app(ty_[], cd)) → new_compare13(vz3500, vz35100, cd)
new_compare(vz340, vz3500, ty_Integer) → new_compare4(vz340, vz3500)
new_merge1(vz34, vz350, [], ba) → new_merge2(vz34, vz350, ba)
new_compare14(vz3500, vz35100, app(ty_Maybe, bf)) → new_compare9(vz3500, vz35100, bf)
new_merge2(:(vz340, vz341), :(vz3500, vz3501), ba) → new_merge00(vz3500, vz340, vz341, vz3501, new_compare(vz340, vz3500, ba), ba)
new_compare(vz340, vz3500, ty_Int) → new_compare5(vz340, vz3500)
new_compare14(vz3500, vz35100, app(app(ty_Either, bg), bh)) → new_compare10(vz3500, vz35100, bg, bh)
new_compare14(vz3500, vz35100, ty_Int) → new_compare5(vz3500, vz35100)
new_compare11(@0, @0) → EQ
new_merge2(vz34, [], ba) → vz34
new_compare1(vz340, vz3500) → error([])
new_compare6(vz340, vz3500) → error([])
new_compare(vz340, vz3500, ty_@0) → new_compare11(vz340, vz3500)
new_compare(vz340, vz3500, ty_Float) → new_compare7(vz340, vz3500)
new_compare5(vz340, vz3500) → error([])
new_compare14(vz3500, vz35100, ty_@0) → new_compare11(vz3500, vz35100)
new_compare12(vz340, vz3500, ca, cb, cc) → error([])
new_compare9(vz340, vz3500, bf) → error([])
new_compare(vz340, vz3500, app(ty_[], cd)) → new_compare13(vz340, vz3500, cd)
new_compare14(vz3500, vz35100, app(ty_Ratio, bc)) → new_compare2(vz3500, vz35100, bc)
new_merge00(vz44, vz45, vz46, vz47, EQ, bb) → :(vz45, new_merge2(vz46, :(vz44, vz47), bb))
new_compare14(vz3500, vz35100, ty_Integer) → new_compare4(vz3500, vz35100)

The set Q consists of the following terms:

new_compare3(x0, x1)
new_compare2(x0, x1, x2)
new_compare9(x0, x1, x2)
new_compare7(x0, x1)
new_compare(x0, x1, ty_Int)
new_compare4(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_compare5(x0, x1)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, ty_Bool)
new_compare1(x0, x1)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge2([], :(x0, x1), x2)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare(x0, x1, ty_Float)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare(x0, x1, ty_Ordering)
new_compare14(x0, x1, ty_Bool)
new_compare6(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_merge00(x0, x1, x2, x3, EQ, x4)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, ty_@0)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, app(ty_Ratio, x2))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, ty_@0)
new_compare12(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_merge_pairs0([], x0)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, ty_Char)
new_compare14(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, ty_Ordering)
new_compare0(x0, x1)
new_compare11(@0, @0)
new_compare8(x0, x1, x2, x3)
new_compare(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, x2, x3)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare14(x0, x1, ty_Integer)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_Int)
new_compare13(x0, x1, x2)
new_compare14(x0, x1, ty_Float)
new_merge_pairs0(:(x0, []), x1)
new_merge1(x0, [], :(x1, x2), x3)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, ty_Double)
new_compare(x0, x1, ty_Integer)
new_merge2(x0, [], x1)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

case	cmp x y of
	GT	→ y : merge cmp (x : xs) ys
	_	→ x : merge cmp xs (y : ys)

merge0	y cmp x xs ys GT	= y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	= x : merge cmp xs (y : ys)